1. Field
This disclosure is generally related to electronic design automation (EDA). More specifically, this disclosure is related to methods and apparatuses for verifying the functionality of a circuit design by using an abstraction-refinement technique.
2. Related Art
Advances in semiconductor fabrication technology have given rise to dramatic increases in the number of transistors per semiconductor device. This increase in transistor count is empowering computer architects to create digital circuit designs with an ever-increasing design complexity. Consequently, as digital circuit designs become more complex, the effort required to verify the correctness of their implementation also becomes more involved.
To verify the functionality of a circuit design, circuit design verification teams typically perform simulation-based verification methods, formal verification methods, or a combination of the two. During simulation-based verification, verification teams typically apply random input stimuli onto a circuit design under verification (CUV) to stimulate the CUV and compare the response from simulation to the expected response. Simulating the CUV against random input stimuli is probabilistic in nature and relies on a high volume of input vectors to achieve a reasonable coverage of the behavior of the CUV. However, as the circuit designs become more complex, the random input stimuli become less effective at covering the important corner cases of the CUV.
During a formal verification, verification teams typically attempt to prove or disprove the correctness of the CUV's functionality. Formal verification typically involves constructing a formal specification and/or a collection of properties that define the correct functionality of the CUV, and then using formal proofs to determine whether the implementation of the CUV satisfies the formal specification and/or the collection of properties. However, formal verification can be computationally expensive unless specific techniques are used to make verification more efficient.
Abstraction-refinement is one such approach which creates an abstract mathematical model of the CUV, and expands the abstract model until the property is satisfied or a counter-example for the CUV is found. Specifically, if the abstraction-refinement procedure determines that the property is satisfied by the abstract model, then it determines that the property is also satisfied by the CUV. On the other hand, if the abstract model becomes functionally equivalent to the CUV, and the formal verification technique finds a counter-example, then the abstraction-refinement procedure determines that the property is not satisfied by the CUV. Unfortunately, even the abstraction-refinement approach can be computationally expensive. Hence, it is desirable to improve the efficiency of formal verification techniques that use abstraction-refinement.